alle-at(es; i; e.P(e)) == e:es-E(es). (loc(e) = i)  P(e) 

latex

---

clarification:

alle-at(es; i; e.P(e)) == e:es-E(es). (es-loc(es; e) = i  Id)  P(e) 

latex

Definitions	x:A. B(x), es-E(es), P  Q, Id, loc(e)
FDL editor aliases	alle-at